Auf Grund der enormen Fortschritte in der Halbleitertechnologie verzeichnet die VLSI-Chip Entwicklung einen Wandel von einer Ära des Mangels an verfügbaren Schaltkreisen zu einer Ära des Überflusses. Diese Entwicklung wird begleitet von einem Übergang von non-queued Systemen zu heavily-queued Systemen in der Schaltungsentwicklung. Diese neuen Systeme zeichnen sich durch deutlich höhere Leistung, drastisch höheren Schaltkreisbedarf und extrem große Zustandsräume aus. Solche Systeme sind mit zufallsgesteuerten Simulationsverfahren, dem derzeitigen Stand der Technik, nicht mehr zu verifizieren.
Mit dem Hochleistungsbeweiser RISC-PaReDuX, der auf der Technologie der Termersetzung beruht, verifizieren wir Schaltungsentwürfe auf einem Netzwerk von Multiprozessoren. Dazu wird das parallele PaReDuX System auf Formeln der Boole'schen Algebra spezialisiert. Somit wird in diesem Projekt ein Beweissystem entwickelt, das auf spezielle Anwendungen hin optimiert werden kann und von der Rechenleistung modernster Rechnerarchitekturen profitiert. Es wurde bereits ein in der Ausbildung eingesetzter Mikroprozessor verifiziert; die Verifikation realistischer industrieller Schaltungen ist in Arbeit.
Dieses Projekt wird seit Ende 1996 von der DFG im Schwerpunktprogramm ,,Deduktion`` gefördert.
Dr. Beatrice Amrhein